Description Logics (DLs) are a family of knowledge representation formalismsmainly characterised by constructors to build complex concepts and roles fromatomic ones. Expressive role constructors are important in many applications,but can be computationally problematical. We present an algorithm that decidessatisfiability of the DL ALC extended with transitive and inverse roles, rolehierarchies, and qualifying number restrictions. Early experiments indicatethat this algorithm is well-suited for implementation. Additionally, we showthat ALC extended with just transitive and inverse roles is still in PSPACE.Finally, we investigate the limits of decidability for this family of DLs.
展开▼
